The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

le(0, y, z) → greater(y, z) [1]
le(s(x), 0, z) → false [1]
le(s(x), s(y), 0) → false [1]
le(s(x), s(y), s(z)) → le(x, y, z) [1]
greater(x, 0) → first [1]
greater(0, s(y)) → second [1]
greater(s(x), s(y)) → greater(x, y) [1]
double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
triple(x) → if(le(x, x, double(x)), x, 0, 0) [1]
if(false, x, y, z) → true [1]
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z)) [1]
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

le(0, y, z) → greater(y, z) [1]
le(s(x), 0, z) → false [1]
le(s(x), s(y), 0) → false [1]
le(s(x), s(y), s(z)) → le(x, y, z) [1]
greater(x, 0) → first [1]
greater(0, s(y)) → second [1]
greater(s(x), s(y)) → greater(x, y) [1]
double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
triple(x) → if(le(x, x, double(x)), x, 0, 0) [1]
if(false, x, y, z) → true [1]
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z)) [1]
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z) [1]

The TRS has the following type information:

le :: 0:s → 0:s → 0:s → false:first:second 0 :: 0:s greater :: 0:s → 0:s → false:first:second s :: 0:s → 0:s false :: false:first:second first :: false:first:second second :: false:first:second double :: 0:s → 0:s triple :: 0:s → true if :: false:first:second → 0:s → 0:s → 0:s → true true :: true

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: le(0, y, z) → greater(y, z) [1] le(s(x), 0, z) → false [1] le(s(x), s(y), 0) → false [1] le(s(x), s(y), s(z)) → le(x, y, z) [1] greater(x, 0) → first [1] greater(0, s(y)) → second [1] greater(s(x), s(y)) → greater(x, y) [1] double(0) → 0 [1] double(s(x)) → s(s(double(x))) [1] triple(x) → if(le(x, x, double(x)), x, 0, 0) [1] if(false, x, y, z) → true [1] if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z)) [1] if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z) [1] The TRS has the following type information: le :: 0:s → 0:s → 0:s → false:first:second 0 :: 0:s greater :: 0:s → 0:s → false:first:second s :: 0:s → 0:s false :: false:first:second first :: false:first:second second :: false:first:second double :: 0:s → 0:s triple :: 0:s → true if :: false:first:second → 0:s → 0:s → 0:s → true true :: true Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
false => 0
first => 1
second => 2
true => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

double(z') -{ 1 }→ 0 :|: z' = 0
double(z') -{ 1 }→ 1 + (1 + double(x)) :|: z' = 1 + x, x >= 0
greater(z', z'') -{ 1 }→ greater(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y
greater(z', z'') -{ 1 }→ 2 :|: y >= 0, z'' = 1 + y, z' = 0
greater(z', z'') -{ 1 }→ 1 :|: z'' = 0, z' = x, x >= 0
if(z', z'', z1, z2) -{ 1 }→ if(le(1 + x, y, 1 + z), 1 + x, y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1
if(z', z'', z1, z2) -{ 1 }→ if(le(1 + x, 1 + y, z), 1 + x, 1 + y, z) :|: z1 = y, z >= 0, z' = 2, z2 = z, x >= 0, y >= 0, z'' = x
if(z', z'', z1, z2) -{ 1 }→ 0 :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
le(z', z'', z1) -{ 1 }→ le(x, y, z) :|: z' = 1 + x, z >= 0, x >= 0, y >= 0, z'' = 1 + y, z1 = 1 + z
le(z', z'', z1) -{ 1 }→ greater(y, z) :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0
le(z', z'', z1) -{ 1 }→ 0 :|: z'' = 0, z' = 1 + x, z1 = z, z >= 0, x >= 0
le(z', z'', z1) -{ 1 }→ 0 :|: z' = 1 + x, z1 = 0, x >= 0, y >= 0, z'' = 1 + y
triple(z') -{ 1 }→ if(le(x, x, double(x)), x, 0, 0) :|: z' = x, x >= 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V18),0,[le(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(start(V, V1, V2, V18),0,[greater(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V18),0,[double(V, Out)],[V >= 0]). eq(start(V, V1, V2, V18),0,[triple(V, Out)],[V >= 0]). eq(start(V, V1, V2, V18),0,[if(V, V1, V2, V18, Out)],[V >= 0,V1 >= 0,V2 >= 0,V18 >= 0]). eq(le(V, V1, V2, Out),1,[greater(V3, V4, Ret)],[Out = Ret,V2 = V4,V4 >= 0,V1 = V3,V3 >= 0,V = 0]). eq(le(V, V1, V2, Out),1,[],[Out = 0,V1 = 0,V = 1 + V5,V2 = V6,V6 >= 0,V5 >= 0]). eq(le(V, V1, V2, Out),1,[],[Out = 0,V = 1 + V7,V2 = 0,V7 >= 0,V8 >= 0,V1 = 1 + V8]). eq(le(V, V1, V2, Out),1,[le(V9, V10, V11, Ret1)],[Out = Ret1,V = 1 + V9,V11 >= 0,V9 >= 0,V10 >= 0,V1 = 1 + V10,V2 = 1 + V11]). eq(greater(V, V1, Out),1,[],[Out = 1,V1 = 0,V = V12,V12 >= 0]). eq(greater(V, V1, Out),1,[],[Out = 2,V13 >= 0,V1 = 1 + V13,V = 0]). eq(greater(V, V1, Out),1,[greater(V14, V15, Ret2)],[Out = Ret2,V = 1 + V14,V14 >= 0,V15 >= 0,V1 = 1 + V15]). eq(double(V, Out),1,[],[Out = 0,V = 0]). eq(double(V, Out),1,[double(V16, Ret11)],[Out = 2 + Ret11,V = 1 + V16,V16 >= 0]). eq(triple(V, Out),1,[double(V17, Ret02),le(V17, V17, Ret02, Ret0),if(Ret0, V17, 0, 0, Ret3)],[Out = Ret3,V = V17,V17 >= 0]). eq(if(V, V1, V2, V18, Out),1,[],[Out = 0,V2 = V19,V20 >= 0,V18 = V20,V21 >= 0,V19 >= 0,V1 = V21,V = 0]). eq(if(V, V1, V2, V18, Out),1,[le(1 + V22, V23, 1 + V24, Ret01),if(Ret01, 1 + V22, V23, 1 + V24, Ret4)],[Out = Ret4,V2 = V23,V24 >= 0,V18 = V24,V22 >= 0,V23 >= 0,V1 = V22,V = 1]). eq(if(V, V1, V2, V18, Out),1,[le(1 + V25, 1 + V26, V27, Ret03),if(Ret03, 1 + V25, 1 + V26, V27, Ret5)],[Out = Ret5,V2 = V26,V27 >= 0,V = 2,V18 = V27,V25 >= 0,V26 >= 0,V1 = V25]). input_output_vars(le(V,V1,V2,Out),[V,V1,V2],[Out]). input_output_vars(greater(V,V1,Out),[V,V1],[Out]). input_output_vars(double(V,Out),[V],[Out]). input_output_vars(triple(V,Out),[V],[Out]). input_output_vars(if(V,V1,V2,V18,Out),[V,V1,V2,V18],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [double/2]
1. recursive : [greater/3]
2. recursive : [le/4]
3. recursive : [if/5]
4. non_recursive : [triple/2]
5. non_recursive : [start/4]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into double/2
1. SCC is partially evaluated into greater/3
2. SCC is partially evaluated into le/4
3. SCC is partially evaluated into if/5
4. SCC is partially evaluated into triple/2
5. SCC is partially evaluated into start/4

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations double/2
* CE 15 is refined into CE [20]
* CE 14 is refined into CE [21]


### Cost equations --> "Loop" of double/2
* CEs [21] --> Loop 15
* CEs [20] --> Loop 16

### Ranking functions of CR double(V,Out)
* RF of phase [16]: [V]

#### Partial ranking functions of CR double(V,Out)
* Partial RF of phase [16]:
- RF of loop [16:1]:
V


### Specialization of cost equations greater/3
* CE 13 is refined into CE [22]
* CE 11 is refined into CE [23]
* CE 12 is refined into CE [24]


### Cost equations --> "Loop" of greater/3
* CEs [23] --> Loop 17
* CEs [24] --> Loop 18
* CEs [22] --> Loop 19

### Ranking functions of CR greater(V,V1,Out)
* RF of phase [19]: [V,V1]

#### Partial ranking functions of CR greater(V,V1,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V
V1


### Specialization of cost equations le/4
* CE 10 is refined into CE [25]
* CE 9 is refined into CE [26]
* CE 8 is refined into CE [27]
* CE 7 is refined into CE [28,29,30,31]


### Cost equations --> "Loop" of le/4
* CEs [26] --> Loop 20
* CEs [27] --> Loop 21
* CEs [31] --> Loop 22
* CEs [30] --> Loop 23
* CEs [29] --> Loop 24
* CEs [28] --> Loop 25
* CEs [25] --> Loop 26

### Ranking functions of CR le(V,V1,V2,Out)
* RF of phase [26]: [V,V1,V2]

#### Partial ranking functions of CR le(V,V1,V2,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
V1
V2


### Specialization of cost equations if/5
* CE 19 is refined into CE [32,33,34,35,36,37,38]
* CE 18 is refined into CE [39,40,41,42,43,44,45]
* CE 17 is refined into CE [46]


### Cost equations --> "Loop" of if/5
* CEs [46] --> Loop 27
* CEs [38] --> Loop 28
* CEs [37] --> Loop 29
* CEs [36] --> Loop 30
* CEs [35] --> Loop 31
* CEs [33] --> Loop 32
* CEs [34] --> Loop 33
* CEs [32] --> Loop 34
* CEs [45] --> Loop 35
* CEs [44] --> Loop 36
* CEs [43] --> Loop 37
* CEs [42] --> Loop 38
* CEs [41] --> Loop 39
* CEs [40] --> Loop 40
* CEs [39] --> Loop 41

### Ranking functions of CR if(V,V1,V2,V18,Out)
* RF of phase [28,30,35,37]: [-2*V1+V2+V18-2]
* RF of phase [29]: [-V1+V18-1,-V2+V18-1]
* RF of phase [38]: [-V1+V2,V2-V18]

#### Partial ranking functions of CR if(V,V1,V2,V18,Out)
* Partial RF of phase [28,30,35,37]:
- RF of loop [28:1]:
-V1+V18-2
-V2+V18-1 depends on loops [35:1,37:1]
- RF of loop [30:1]:
V-1 depends on loops [35:1]
-V1+V18-1
- RF of loop [35:1]:
-V+2 depends on loops [30:1]
- RF of loop [35:1,37:1]:
-V1+V2-1
- RF of loop [37:1]:
V2-V18 depends on loops [28:1,30:1]
* Partial RF of phase [29]:
- RF of loop [29:1]:
-V1+V18-1
-V2+V18-1
* Partial RF of phase [38]:
- RF of loop [38:1]:
-V1+V2
V2-V18


### Specialization of cost equations triple/2
* CE 16 is refined into CE [47,48]


### Cost equations --> "Loop" of triple/2
* CEs [48] --> Loop 42
* CEs [47] --> Loop 43

### Ranking functions of CR triple(V,Out)

#### Partial ranking functions of CR triple(V,Out)


### Specialization of cost equations start/4
* CE 2 is refined into CE [49,50,51,52,53,54,55,56,57,58,59,60]
* CE 3 is refined into CE [61,62,63,64]
* CE 4 is refined into CE [65,66]
* CE 5 is refined into CE [67,68]
* CE 6 is refined into CE [69,70,71,72,73,74,75,76,77,78,79,80,81,82]


### Cost equations --> "Loop" of start/4
* CEs [82] --> Loop 44
* CEs [57] --> Loop 45
* CEs [59] --> Loop 46
* CEs [54] --> Loop 47
* CEs [53,62] --> Loop 48
* CEs [81] --> Loop 49
* CEs [80] --> Loop 50
* CEs [79] --> Loop 51
* CEs [77] --> Loop 52
* CEs [78] --> Loop 53
* CEs [76] --> Loop 54
* CEs [75] --> Loop 55
* CEs [74] --> Loop 56
* CEs [73] --> Loop 57
* CEs [71] --> Loop 58
* CEs [72] --> Loop 59
* CEs [55,56,58,60,63,64,66,68,70] --> Loop 60
* CEs [49,50,51,52,61,65,67,69] --> Loop 61

### Ranking functions of CR start(V,V1,V2,V18)

#### Partial ranking functions of CR start(V,V1,V2,V18)


Computing Bounds
=====================================

#### Cost of chains of double(V,Out):
* Chain [[16],15]: 1*it(16)+1
Such that:it(16) =< Out/2

with precondition: [2*V=Out,V>=1]

* Chain [15]: 1
with precondition: [V=0,Out=0]


#### Cost of chains of greater(V,V1,Out):
* Chain [[19],18]: 1*it(19)+1
Such that:it(19) =< V

with precondition: [Out=2,V>=1,V1>=V+1]

* Chain [[19],17]: 1*it(19)+1
Such that:it(19) =< V1

with precondition: [Out=1,V1>=1,V>=V1]

* Chain [18]: 1
with precondition: [V=0,Out=2,V1>=1]

* Chain [17]: 1
with precondition: [V1=0,Out=1,V>=0]


#### Cost of chains of le(V,V1,V2,Out):
* Chain [[26],25]: 1*it(26)+2
Such that:it(26) =< V

with precondition: [Out=2,V=V1,V>=1,V2>=V+1]

* Chain [[26],24]: 1*it(26)+2
Such that:it(26) =< V

with precondition: [Out=1,V=V2,V>=1,V1>=V]

* Chain [[26],23]: 1*it(26)+1*s(1)+2
Such that:s(1) =< -V+V2
it(26) =< V

with precondition: [Out=1,V>=1,V2>=V+1,V1>=V2]

* Chain [[26],22]: 1*it(26)+1*s(2)+2
Such that:s(2) =< -V+V1
it(26) =< V

with precondition: [Out=2,V>=1,V1>=V+1,V2>=V1+1]

* Chain [[26],21]: 1*it(26)+1
Such that:it(26) =< V1

with precondition: [Out=0,V1>=1,V>=V1+1,V2>=V1]

* Chain [[26],20]: 1*it(26)+1
Such that:it(26) =< V2

with precondition: [Out=0,V2>=1,V>=V2+1,V1>=V2+1]

* Chain [25]: 2
with precondition: [V=0,V1=0,Out=2,V2>=1]

* Chain [24]: 2
with precondition: [V=0,V2=0,Out=1,V1>=0]

* Chain [23]: 1*s(1)+2
Such that:s(1) =< V2

with precondition: [V=0,Out=1,V2>=1,V1>=V2]

* Chain [22]: 1*s(2)+2
Such that:s(2) =< V1

with precondition: [V=0,Out=2,V1>=1,V2>=V1+1]

* Chain [21]: 1
with precondition: [V1=0,Out=0,V>=1,V2>=0]

* Chain [20]: 1
with precondition: [V2=0,Out=0,V>=1,V1>=1]


#### Cost of chains of if(V,V1,V2,V18,Out):
* Chain [[38],40,27]: 3*it(38)+1*s(3)+1*s(6)+3
Such that:it(38) =< V2-V18
aux(2) =< V2
s(3) =< aux(2)
s(6) =< it(38)*aux(2)

with precondition: [V=1,Out=0,V1=V18,V1>=0,V2>=V1+1]

* Chain [[29],31,40,27]: 3*it(29)+2*s(3)+1*s(10)+6
Such that:it(29) =< -V1+V18
aux(5) =< V18
s(3) =< aux(5)
s(10) =< it(29)*aux(5)

with precondition: [V=2,Out=0,V1=V2,V1>=0,V18>=V1+2]

* Chain [[28,30,35,37],36,31,40,27]: 6*it(28)+6*it(35)+3*s(3)+1*s(28)+1*s(29)+1*s(30)+1*s(31)+1*s(32)+2*s(33)+1*s(34)+9
Such that:aux(28) =< -2*V1+V2+V18
aux(29) =< -V1+V2
aux(30) =< -V1+V2+V18
aux(31) =< -V1+V18
s(3) =< aux(30)
it(28) =< aux(28)
it(35) =< aux(28)
it(35) =< aux(29)
it(28) =< aux(31)
aux(13) =< aux(30)
aux(20) =< aux(31)+1
aux(16) =< aux(29)-1
s(33) =< it(35)*aux(13)
s(34) =< it(35)*aux(20)
s(32) =< it(35)*aux(16)
s(31) =< it(28)*aux(13)
s(30) =< it(28)*aux(31)
s(29) =< it(28)*aux(30)
s(28) =< it(28)*aux(29)

with precondition: [Out=0,2>=V,V>=1,V1>=0,V18>=V+V1,V+V2>=V1+3]

* Chain [41,27]: 3
with precondition: [V=1,V2=0,Out=0,V1>=0,V18>=0]

* Chain [40,27]: 1*s(3)+3
Such that:s(3) =< V2

with precondition: [V=1,Out=0,V2>=1,V1>=V2,V18+1>=V2]

* Chain [39,27]: 1*s(36)+3
Such that:s(36) =< V18+1

with precondition: [V=1,Out=0,V18>=0,V1>=V18+1,V2>=V18+2]

* Chain [36,[29],31,40,27]: 3*it(29)+2*s(3)+1*s(10)+1*s(11)+9
Such that:it(29) =< -V1+V18
s(11) =< V1+1
aux(5) =< V18+1
s(3) =< aux(5)
s(10) =< it(29)*aux(5)

with precondition: [V=1,Out=0,V2=V1+1,V2>=1,V18>=V2+1]

* Chain [36,31,40,27]: 2*s(3)+1*s(11)+9
Such that:s(11) =< V18
aux(3) =< V18+1
s(3) =< aux(3)

with precondition: [V=1,Out=0,V18=V1+1,V18=V2,V18>=1]

* Chain [34,27]: 3
with precondition: [V=2,V18=0,Out=0,V1>=0,V2>=0]

* Chain [33,27]: 1*s(37)+3
Such that:s(37) =< V18

with precondition: [V=2,Out=0,V18>=1,V1>=V18,V2>=V18]

* Chain [32,27]: 1*s(38)+3
Such that:s(38) =< V2+1

with precondition: [V=2,Out=0,V2>=0,V1>=V2+1,V18>=V2+1]

* Chain [31,[38],40,27]: 3*it(38)+1*s(3)+1*s(6)+1*s(7)+6
Such that:aux(2) =< V2+1
it(38) =< V2-V18+1
s(7) =< V18
s(3) =< aux(2)
s(6) =< it(38)*aux(2)

with precondition: [V=2,Out=0,V18=V1+1,V18>=1,V2>=V18]

* Chain [31,40,27]: 2*s(3)+6
Such that:aux(3) =< V18
s(3) =< aux(3)

with precondition: [V=2,Out=0,V18=V1+1,V18=V2+1,V18>=1]

* Chain [27]: 1
with precondition: [V=0,Out=0,V1>=0,V2>=0,V18>=0]


#### Cost of chains of triple(V,Out):
* Chain [43]: 7
with precondition: [V=0,Out=0]

* Chain [42]: 2*s(39)+7
Such that:aux(32) =< V
s(39) =< aux(32)

with precondition: [Out=0,V>=1]


#### Cost of chains of start(V,V1,V2,V18):
* Chain [61]: 1*s(41)+1*s(42)+7
Such that:s(42) =< V1
s(41) =< V2

with precondition: [V=0]

* Chain [60]: 2*s(43)+1*s(44)+1*s(45)+6*s(46)+1*s(47)+7
Such that:s(47) =< -V+V1
s(45) =< -V+V2
s(44) =< V2
aux(33) =< V
aux(34) =< V1
s(46) =< aux(33)
s(43) =< aux(34)

with precondition: [V>=1]

* Chain [59]: 1*s(54)+2*s(56)+9
Such that:s(54) =< V18
s(55) =< V18+1
s(56) =< s(55)

with precondition: [V=1,V1+1=V2,V1+1=V18,V1>=0]

* Chain [58]: 3*s(57)+1*s(58)+2*s(60)+1*s(61)+9
Such that:s(57) =< -V2+V18+1
s(58) =< V2
s(59) =< V18+1
s(60) =< s(59)
s(61) =< s(57)*s(59)

with precondition: [V=1,V1+1=V2,V1>=0,V18>=V1+2]

* Chain [57]: 3*s(62)+1*s(64)+1*s(65)+3
Such that:s(63) =< V2
s(62) =< V2-V18
s(64) =< s(63)
s(65) =< s(62)*s(63)

with precondition: [V=1,V1=V18,V1>=0,V2>=V1+1]

* Chain [56]: 1*s(66)+3
Such that:s(66) =< V2

with precondition: [V=1,V2>=1,V1>=V2,V18+1>=V2]

* Chain [55]: 1*s(67)+3
Such that:s(67) =< V18+1

with precondition: [V=1,V18>=0,V1>=V18+1,V2>=V18+2]

* Chain [54]: 3
with precondition: [V=2,V18=0,V1>=0,V2>=0]

* Chain [53]: 3*s(69)+1*s(70)+1*s(71)+1*s(72)+6
Such that:s(68) =< V2+1
s(69) =< V2-V18+1
s(70) =< V18
s(71) =< s(68)
s(72) =< s(69)*s(68)

with precondition: [V=2,V1+1=V18,V1>=0,V2>=V1+1]

* Chain [52]: 2*s(74)+6
Such that:s(73) =< V18
s(74) =< s(73)

with precondition: [V=2,V1=V2,V1+1=V18,V1>=0]

* Chain [51]: 3*s(75)+2*s(77)+1*s(78)+6
Such that:s(75) =< -V1+V18
s(76) =< V18
s(77) =< s(76)
s(78) =< s(75)*s(76)

with precondition: [V=2,V1=V2,V1>=0,V18>=V1+2]

* Chain [50]: 1*s(79)+3
Such that:s(79) =< V2+1

with precondition: [V=2,V2>=0,V1>=V2+1,V18>=V2+1]

* Chain [49]: 1*s(80)+3
Such that:s(80) =< V18

with precondition: [V=2,V18>=1,V1>=V18,V2>=V18]

* Chain [48]: 1
with precondition: [V1=0,V>=0]

* Chain [47]: 1
with precondition: [V2=0,V>=1,V1>=1]

* Chain [46]: 1*s(81)+2
Such that:s(81) =< V1

with precondition: [V=V1,V>=1,V2>=V+1]

* Chain [45]: 1*s(82)+2
Such that:s(82) =< V2

with precondition: [V=V2,V>=1,V1>=V]

* Chain [44]: 3*s(87)+6*s(88)+6*s(89)+2*s(93)+1*s(94)+1*s(95)+1*s(96)+1*s(97)+1*s(98)+1*s(99)+9
Such that:s(83) =< -2*V1+V2+V18
s(84) =< -V1+V2
s(85) =< -V1+V2+V18
s(86) =< -V1+V18
s(87) =< s(85)
s(88) =< s(83)
s(89) =< s(83)
s(89) =< s(84)
s(88) =< s(86)
s(90) =< s(85)
s(91) =< s(86)+1
s(92) =< s(84)-1
s(93) =< s(89)*s(90)
s(94) =< s(89)*s(91)
s(95) =< s(89)*s(92)
s(96) =< s(88)*s(90)
s(97) =< s(88)*s(86)
s(98) =< s(88)*s(85)
s(99) =< s(88)*s(84)

with precondition: [2>=V,V>=1,V1>=0,V18>=V+V1,V+V2>=V1+3]


Closed-form bounds of start(V,V1,V2,V18):
-------------------------------------
* Chain [61] with precondition: [V=0]
- Upper bound: nat(V1)+7+nat(V2)
- Complexity: n
* Chain [60] with precondition: [V>=1]
- Upper bound: 6*V+7+nat(V1)*2+nat(V2)+nat(-V+V1)+nat(-V+V2)
- Complexity: n
* Chain [59] with precondition: [V=1,V1+1=V2,V1+1=V18,V1>=0]
- Upper bound: 3*V18+11
- Complexity: n
* Chain [58] with precondition: [V=1,V1+1=V2,V1>=0,V18>=V1+2]
- Upper bound: V2+2*V18+11+ (-V2+V18+1)* (V18+1)+ (-3*V2+3*V18+3)
- Complexity: n^2
* Chain [57] with precondition: [V=1,V1=V18,V1>=0,V2>=V1+1]
- Upper bound: 3*V2-3*V18+ (V2+3+ (V2-V18)*V2)
- Complexity: n^2
* Chain [56] with precondition: [V=1,V2>=1,V1>=V2,V18+1>=V2]
- Upper bound: V2+3
- Complexity: n
* Chain [55] with precondition: [V=1,V18>=0,V1>=V18+1,V2>=V18+2]
- Upper bound: V18+4
- Complexity: n
* Chain [54] with precondition: [V=2,V18=0,V1>=0,V2>=0]
- Upper bound: 3
- Complexity: constant
* Chain [53] with precondition: [V=2,V1+1=V18,V1>=0,V2>=V1+1]
- Upper bound: 3*V2-3*V18+3+ (V2+V18+7+ (V2-V18+1)* (V2+1))
- Complexity: n^2
* Chain [52] with precondition: [V=2,V1=V2,V1+1=V18,V1>=0]
- Upper bound: 2*V18+6
- Complexity: n
* Chain [51] with precondition: [V=2,V1=V2,V1>=0,V18>=V1+2]
- Upper bound: 2*V18+6+ (-V1+V18)*V18+ (-3*V1+3*V18)
- Complexity: n^2
* Chain [50] with precondition: [V=2,V2>=0,V1>=V2+1,V18>=V2+1]
- Upper bound: V2+4
- Complexity: n
* Chain [49] with precondition: [V=2,V18>=1,V1>=V18,V2>=V18]
- Upper bound: V18+3
- Complexity: n
* Chain [48] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
* Chain [47] with precondition: [V2=0,V>=1,V1>=1]
- Upper bound: 1
- Complexity: constant
* Chain [46] with precondition: [V=V1,V>=1,V2>=V+1]
- Upper bound: V1+2
- Complexity: n
* Chain [45] with precondition: [V=V2,V>=1,V1>=V]
- Upper bound: V2+2
- Complexity: n
* Chain [44] with precondition: [2>=V,V>=1,V1>=0,V18>=V+V1,V+V2>=V1+3]
- Upper bound: (-V1+V2-1)* (-2*V1+V2+V18)+9+ (-2*V1+V2+V18)* (-V1+V2)+ (-2*V1+V2+V18)* (-2*V1+2*V18)+ (-3*V1+3*V2+3*V18)+ (-2*V1+V2+V18)* (-4*V1+4*V2+4*V18)+ (-26*V1+13*V2+13*V18)
- Complexity: n^2

### Maximum cost of start(V,V1,V2,V18): max([max([max([2,nat(V1)+1,nat(V2+1)+2,nat(V18+1)+2,nat(-2*V1+V2+V18)*nat(nat(-V1+V2)+ -1)+8+nat(-2*V1+V2+V18)*nat(-V1+V2)+nat(-V1+V18)*2*nat(-2*V1+V2+V18)+nat(-V1+V2+V18)*3+nat(-V1+V2+V18)*4*nat(-2*V1+V2+V18)+nat(-2*V1+V2+V18)*13]),nat(V18)+2+max([max([nat(V18+1)*2+6,nat(V2+1)+3+nat(V2-V18+1)*nat(V2+1)+nat(V2-V18+1)*3]),nat(-V1+V18)*nat(V18)+nat(-V1+V18)*3+ (nat(V18)+3)])]),nat(V2)+1+max([max([1,nat(V2-V18)*nat(V2)+1+nat(V2-V18)*3,nat(V18+1)*2+7+nat(-V2+V18+1)*nat(V18+1)+nat(-V2+V18+1)*3]),6*V+nat(V1)+nat(-V+V1)+nat(-V+V2)+ (nat(V1)+5)])])+1
Asymptotic class: n^2
* Total analysis performed in 1192 ms.

(10) BOUNDS(1, n^2)